p{-}filter($f$)($x$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$case $f$($x$) of inl($p$) =$>$ inl $x$  $\mid$ inr($p$) =$>$ inr $p$